Nuprl Definition : R-da
11,40
postcript
pdf
R-da(
R
;
i
)
== es_realizer_ind(
R
;
== es_realizer_ind(
fpf-empty;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.fpf-join(Kind-deq;
rec1
;
rec2
);
== es_realizer_ind(
loc
,
T
,
x
,
v
.fpf-empty;
== es_realizer_ind(
loc
,
T
,
x
,
L
.fpf-empty;
== es_realizer_ind(
lnk
,
tag
,
L
.fpf-empty;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.if eq_id(
loc
;
i
) then fpf-single(
knd
;
T
) else fpf-empty fi ;
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.if eq_id(source(
l
);
i
)
== es_realizer_ind(
then fpf-join(Kind-deq; fpf-single(
knd
;
T
); lnk-decl(
l
;
dt
))
== es_realizer_ind(
else fpf-empty
== es_realizer_ind(
fi ;
== es_realizer_ind(
loc
,
ds
,
a
,
p
,
P
.if eq_id(
loc
;
i
)
== es_realizer_ind(
then fpf-single(locl(
a
); p-outcome(
p
))
== es_realizer_ind(
else fpf-empty
== es_realizer_ind(
fi ;
== es_realizer_ind(
loc
,
k
,
L
.fpf-empty;
== es_realizer_ind(
loc
,
k
,
L
.fpf-empty;
== es_realizer_ind(
loc
,
x
,
L
.fpf-empty)
latex
Definitions
fpf-empty
,
p-outcome(
p
)
,
locl(
a
)
,
fpf-single(
x
;
v
)
,
eq_id(
a
;
b
)
,
if
b
then
t
else
f
fi
,
lnk-decl(
l
;
dt
)
,
Kind-deq
,
fpf-join(
eq
;
f
;
g
)
,
source(
l
)
,
es
realizer
ind
FDL editor aliases
R-da
origin